$\vdash$  $\forall$$P$:($\mathbb{N}\rightarrow\mathbb{B}$). Dec($\exists$$n$:$\mathbb{N}$. ($\uparrow$($P$($n$)))) $\Rightarrow$ ($\exists$$x$:$\mathbb{N}$ + Top. p{-}mu($P$;$x$))